Дифференциальная геометрия

Четвертая полка моей библиотеки посвящена дифференциальной геометрии — той математике, теоремы в которой приобретают компактный и непосредственный вид, и выглядят как продолжение теории гомотопических лимитов и колимитов. Введение в формализацию современной дифференциальной геометрии в модальной HoTT можно получить из диссертации Феликса Веллена. Немного про конференцию по дифференциальной геометрии в HoTT.

Кроме МГУ курса Постникова рекомендую ознакомиться с геометрической теорией интегрирования и когомологиями де Рама, а также введением в теорию схем Хартсхорна, как подготовке к Stack Project.

Дифференциальная геометрия 514.7

Дифференциальная геометрия и топология. Дополнительные главы.
А.Фоменко. 1986. УДК 514
Лекции по геометрии. Семестр 1. Аналитическая геометрия.
М.Постников. 1982. УДК 514.12
Лекции по геометрии. Семестр 2. Линейная алгебра.
М.Постников. 1986. УДК 512.64
Лекции по геометрии. Семестр 3. Гладкие многообразия.
М.Постников. 1987. УДК 515.12
Лекции по геометрии. Семестр 4. Дифференциальная геометрия.
М.Постников. 1988. УДК 514.7
Лекции по геометрии. Семестр 5. Группы и алгебры Ли.
М.Постников. 1982. УДК 514
Дифференциальное исчисление. Дифференциальные формы.
А.Картан. 1971. УДК 514.7 + 517.43
Лекции по дифференциальной геометрии. С.Стернберг. 1970. УДК 514.7
Основания дифференциальной геометрии. О.Веблен, Дж.Уайтхед. 1949. УДК 514.7
Дифференциируемые многообразия. Ж. де Рам. 1956. УДК 514.7
Характеристические классы. Дж.Милнор, Дж.Сташеф. 1979. УДК 515.2 + 514.77
Элементы дифференциальной геометрии и топологии.
С.Новиков, А.Фоменко. 1987. УДК 515.2 + 514.77
Элементы топологии и дифференциируемые многообразия.
К.Телеман. 1967. УДК 514.77 + 519.49
Алгебраическая геометрия. Р.Хартсхорн. 1981. УДК 514.7
Геометрическая теория интегрирования. Х.Уитни. 1960. УДК 514.7
Алгебраические группы и поля классов. Ж.Серр. 1968. УДК 512.7 + 514.7
Группы преобразований в дифференциальной геометрии. Ш.Кобаяси. 1986. УДК 514.7
Основы алгебраической геометрии. И.Шафаревич. 2007. УДК 512.7

Если этого мало, то всегда можно взять построить из этого топосы, перейти к геометрическим морфизмам между ними и выйти таким образом в модальный сеттинг. Теория схем Шевалле-Гротендика поможет вам связать алгебраическую геометорию и дифференциальную геометорию, ну а оттуда уже сразу в теорию стеков и престек функториальную теорию типов, в которой контексты строятся не на сигмах, а на конструкциях Гротендика.